$\forall$$A$:Type, $I$:MaInterface($A$), $i$:\{$i$:Id$\mid$ ($i$ $\in$ fpf{-}domain($I$))\} .
\\[0ex]($I$($i$).2) $\in$ $k$:\{$k$:Knd$\mid$ $\uparrow$hasloc($k$;$i$)\}  fp$\rightarrow$ $V$:Type $\times$ Top